COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00003 00003	
 00004 ENDMK
⊗;





.BEGIN CENTER





PRELIMINARY USER'S MANUAL
FOR
INTERACTIVE THEOREM PROVER

BY

JOHN ALLEN
.END






.BEGIN CENTER




Preface
.END

.BEGIN DOUBLE SPACE
This document represents a short guide to using a development of the program
originally described in Allen and Luckham [MI5].  Many of the later sections
,on pattern matching and subroutining especially, are still in a rudimentary
stage of development. Experiments demonstrating various applications of the strategies
and the user oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and Morales.
.END